COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	lisp book to Sten-Ake
C00007 ENDMK
C⊗;
lisp book to Sten-Ake
address change for Stoyan

Please put her on the list for the my next paper on circumscription.
Mary-Angela Papalaskaris
Dept. of Artificial Intelligence
Edinburgh University
Hope Park Square
Edinburgh EH89NW
Scotland

Peter Thieriot, President Chronicle Information Systems
may call about Videotex

1/2 page about what science and labor should do together. - FOR CHUDNOVSKY

*****

What higher nervous systems must do is determined by the information-processing
problems they must solve. - David Marr

	We humans live in a world in which we have very limited access
to many kinds of information.  We can only see parts of objects.  We
have limited information about the laws of motion.  We have limited
information about the states of mind of the people with whom we
interact.  We even have limited information about our own states
of mind.  We also have a limited ability to remember and compute.

	We have evolved intellectual mechanisms for achieving our
goals, in so far as they can be achieved, within these limitations.
Machines will have similar limitations.  To a substantial extent,
the ideas we have and the methods we use are determined by the
problems we must solve and the information we have to solve them.
All this is just spelling out the point made in the above quotation
from David Marr.

	My approach then is to study what intellectual mechanisms
will work to solve the intellectual problems.  Except for mechanisms
involving heavy computing, which have so far been rather specialized in their
applicability, we haven't discovered any intellectual mechanisms not
also used by humans.

****

true all(var,propform) ⊃ ∀t.term t ⊃ true subst(t,var,propform)

If we have terms for all the elements of the domain we can write

true all(var,propform) ≡ ∀t.term t ⊃ true subst(t,var,propform)

The explicit use of  subst  keeps everything genuinely first order.

vars propform

value(propform,structure)  is a proposition

true all(var,propform) ≡
 ∀x structure.x ε domain ∧ val(var,structure) = x ⊃ true value(propform,structure)

****

It is our intuition that forward and backward chaining are mutually
reducible.  It requires reification.

To reduce backward chaining to forward chaining, we use the
axiom

want q ∧ true(p implies q) ⊃ want p

and introduce the goal p by the statement  want p.

To go the other way we introduce the goal true x and the axiom

true p and true(p implies q) 

This isn't quite right, because we would then be satisfied with the
initial true statement.

1983 Nov 17
Bill Turner, 914 945-2045 called from IBM Yorktown to ask about
what Stoyan told me about East German use of IBM computer in Karl Marx Stadt.